Инвариант класса

В программировании, в частности объектно-ориентированном программировании, инвариант класса (или инвариант типа) — инвариант, используемый для ограничения объектов класса. Методы класса должны сохранять инвариант.

Во время создания классов устанавливаются их инварианты, которые постоянно поддерживаются между вызовами публичных методов. Временное нарушение классовой инвариантности между частными вызовами метода возможно, хотя и нежелательно.

Инвариант объекта представляет собой конструкцию программирования, состоящую из набора инвариантных свойств. Это гарантирует, что объект всегда будет соответствовать предопределенным условиям, и поэтому методы могут всегда ссылаться на объект без риска сделать неточные презумпции. Определение инвариантов классов может помочь программистам и тестировщикам обнаружить больше ошибок при тестировании программного обеспечения.

Инварианты классов и наследование

Полезный эффект инвариантов класса в объектно-ориентированном программировании увеличивается при наличии наследования. Инварианты класса наследуются, то есть инварианты всех родителей класса относятся к самому классу.

Наследование позволяет классам-потомкам изменять данные реализации родительских классов, поэтому класс потомков может изменять состояние экземпляров таким образом, чтобы сделать их недействительными с точки зрения родительского класса. Обращение к этому типу неверного потомка является одной из причин, по которой объектно-ориентированные разработчики программного обеспечения дают предпочтение инкапсуляции наследованию.

Однако, поскольку инварианты класса наследуются, инвариант класса для любого конкретного класса состоит из любых инвариантных утверждений, закодированных непосредственно в этом классе, совмещено со всеми инвариантными предложениями, унаследованными от родителей этого класса. Это означает, что, хотя классы потомков могут иметь доступ к данным реализации своих родителей, инвариант класса может помешать им манипулировать этими данными любым способом, который создаёт недопустимый экземпляр во время выполнения.

Поддержка языков программирования

Утверждения

Такие языки программирования, как C++ и Java, поддерживают утверждения по умолчанию, что может использоваться для определения инвариантов класса. Общим примером реализации инвариантов в классах является то, что конструктор класса генерирует исключение, если инвариант не выполняется. Поскольку методы сохраняют инварианты, они могут принять справедливость инварианта и не должны явно проверять его.

Родная поддержка

Инвариант класса является существенным компонентом контрактного программирования. Таким образом, языки программирования, обеспечивающие полную поддержку контрактного программирования, такие как Eiffel, Ада и D, также будут обеспечивать полную поддержку инвариантов классов.

Неродная поддержка

В Java существует более мощный инструмент, называемый Java Modeling Language, который обеспечивает более надежный способ определения инвариантов класса.

Примеры

Родная поддержка

D

Язык программирования D имеет встроенную поддержку инвариантов класса, а также другие методы программирования контрактов. Вот пример из официальной документации.

class Date {
  int day;
  int hour;

  invariant() {
    assert(1 <= day && day <= 31);
    assert(0 <= hour && hour < 24);
  }
}

Eiffel

В Eiffel инвариант класса объявляется в конце класса после ключевого слова.

class
	DATE

create
	make

feature {NONE} -- Initialization

	make (a_day: INTEGER; a_hour: INTEGER)
			-- Initialize `Current' with `a_day' and `a_hour'.
		require
			valid_day: 1 <= a_day and a_day <= 31
			valid_hour: 0 <= a_hour and a_hour <= 23
		do
			day := a_day
			hour := a_hour
		ensure
			day_set: day = a_day
			hour_set: hour = a_hour
		end

feature -- Access

	day: INTEGER
		-- Day of month for `Current'

	hour: INTEGER
		-- Hour of day for `Current'

feature -- Element change

	set_day (a_day: INTEGER)
			-- Set `day' to `a_day'
		require
			valid_argument: 1 <= a_day and a_day <= 31
		do
			day := a_day
		ensure
			day_set: day = a_day
		end

	set_hour (a_hour: INTEGER)
			-- Set `hour' to `a_hour'
		require
			valid_argument: 0 <= a_hour and a_hour <= 23
		do
			hour := a_hour
		ensure
			hour_set: hour = a_hour
		end

invariant
	valid_day: 1 <= day and day <= 31
	valid_hour: 0 <= hour and hour <= 23
end

Неродная поддержка

Java

Это пример инварианта класса в языке программирования Java с Java Modeling Language. Инвариант должен иметь значение true после завершения конструктора и при входе, и выходе всех членов публичной функции, которые должны определять предварительное условие и постусловие, чтобы обеспечить инвариант класса.

public class Date {
    int /*@spec_public@*/ day;
    int /*@spec_public@*/ hour;

    /*@invariant 1 <= day && day <= 31; @*/ //class invariant
    /*@invariant 0 <= hour && hour < 24; @*/ //class invariant

    /*@
    @requires 1 <= d && d <= 31;
    @requires 0 <= h && h < 24;
    @*/
    public Date(int d, int h) { // constructor
        day = d;
        hour = h;
    }

    /*@
    @requires 1 <= d && d <= 31;
    @ensures day == d;
    @*/
    public void setDay(int d) {
        day = d;
    }

    /*@
    @requires 0 <= h && h < 24;
    @ensures hour == h;
    @*/
    public void setHour(int h) {
        hour = h;
    }
}